\begin{tabbing} $\vdash$ \=$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).\+ \\[0ex]Trans($T$;$a$,$b$.$R$($a$,$b$)) \\[0ex]$\Rightarrow$ \{$\forall$$a$, $b$, $c$:$T$. $R$($a$,$b$) $\Rightarrow$ strict\_part($x$,$y$.$R$($x$,$y$);$b$;$c$) $\Rightarrow$ strict\_part($x$,$y$.$R$($x$,$y$);$a$;$c$)\} \- \end{tabbing}